Nuprl Definition : R-state-var
11,40
postcript
pdf
R-state-var(
i
;
ds
;
da
;
x
;
T
;
ks
;
tr
)
== Rplus(Rall(
ks
;
== Rplus(Rall(
k
.Reffect(
i
;
== Rplus(Rall(
k
.Reffect(
fpf-join(id-deq;
ds
; fpf-single(
x
;
T
));
== Rplus(Rall(
k
.Reffect(
k
;
== Rplus(Rall(
k
.Reffect(
ma-valtype(
da
;
k
);
== Rplus(Rall(
k
.Reffect(
x
;
== Rplus(Rall(
k
.Reffect(
(inl (
s
,
v
.
tr
(
k
,
s
,
v
,
s
(
x
))) )));
== Rplus(
Rframe(
i
;
T
;
x
;
ks
))
latex
Definitions
fpf-join(
eq
;
f
;
g
)
,
id-deq
,
fpf-single(
x
;
v
)
,
ma-valtype(
da
;
k
)
,
inl
x
,
x
.
A
(
x
)
,
f
(
a
)
FDL editor aliases
R-state-var
origin